A:Type, eq:EqDecider(A), B:(AType), x, y:A, v:B(x), u:B(y).
x : v || y : u  ((x = y)  (v = u  B(x))) 

latex

Definitions	t  T, x(s), x:A. B(x), EqDecider(T), , P  Q, x. t(x), f || g, P  Q, x : v, a:A fp B(a), P & Q, P  Q, b, Top
Lemmas	fpf-single-dom-sq, deq property, fpf-compatible wf, fpf-single wf, fpf-compatible-singles, deq wf, subtype rel self